Skip to content

feat(Fork): complete forking lemma proof with seeded oracle infrastructure#113

Merged
quangvdao merged 3 commits intomasterfrom
quang/finish-forking
Mar 1, 2026
Merged

feat(Fork): complete forking lemma proof with seeded oracle infrastructure#113
quangvdao merged 3 commits intomasterfrom
quang/finish-forking

Conversation

@quangvdao
Copy link
Collaborator

@quangvdao quangvdao commented Mar 1, 2026 •
edited
Loading

Summary

This PR completes the formal proof of the forking lemma, a key tool in provable security for bounding the success probability of "fork-and-replay" reductions.

Forking lemma (Fork.lean, +295 lines)

  • le_probOutput_fork: per-index lower bound showing Pr[cf(main) = s]² - Pr[cf(main) = s] / |Range i| ≤ Pr[fork succeeds at s]
  • probOutput_none_fork_le: main failure-probability bound Pr[fork fails] ≤ 1 - acc * (acc / q - 1/h)
  • Supporting lemmas: collision-guard bound (probOutput_collision_le_main_div), no-guard factorization, and the Cauchy-Schwarz / Jensen step via prefix grouping

Seeded oracle faithfulness (SeededOracle.lean, +628 lines)

  • evalDist_liftComp_generateSeed_bind_simulateQ_run': seeded simulation preserves distributions (the core faithfulness theorem)
  • evalDist_liftComp_uniformSample_bind_simulateQ_run'_addValue: adding a uniform value to a seed doesn't change the distribution
  • evalDist_liftComp_generateSeed_bind_simulateQ_run'_takeAtIndex: truncating the seed preserves distributions
  • tsum_probOutput_generateSeed_weight_takeAtIndex: weighted faithfulness for prefix-dependent weights (used in the Jensen step)
  • generateSeedCounts: product seed generator with explicit per-index counts and full support characterization

QuerySeed operations (Structures.lean, +54 lines)

  • pop, prependValues, takeAtIndex with simp lemmas, injectivity, and round-trip properties

ENNReal inequalities (SumSquares.lean, +44 lines, new file)

  • sq_tsum_le_tsum_sq: Cauchy-Schwarz for weighted ℝ≥0∞ tsum
  • sq_sum_le_card_mul_sum_sq: finite Cauchy-Schwarz for ℝ≥0∞ sums

Other

  • Minor Fiat-Shamir proof updates for compatibility
  • Co-authorship headers updated across 24 files with significant contributions

Test plan

  • lake build passes
  • No sorry in any changed file
  • All linter warnings resolved

@quangvdao
feat(crypto): prove Fiat-Shamir lift execution and advance forking proof
df65d1a 
Close `FiatShamir.exec_lift_probComp` and replace the forking lemma checkpoint with a full bound decomposition proof, leaving only the core square-bound subgoal for follow-up.

Made-with: Cursor
@quangvdao
feat(Fork): complete forking lemma proof and seeded oracle infrastruc…
d826265 
…ture

Prove the full forking lemma (`le_probOutput_fork`, `probOutput_none_fork_le`)
by establishing seeded oracle faithfulness, the addValue/takeAtIndex factorization
lemmas, and a Cauchy-Schwarz bound for ENNReal tsum. Also adds QuerySeed operations
(pop, prependValues, takeAtIndex) and the generateSeedCounts seed generator.

Made-with: Cursor
@github-actions
Copy link

github-actions bot commented Mar 1, 2026

🤖 AI-Generated PR Summary

Files Changed:

  • ToMathlib/Data/ENNReal/SumSquares.lean
  • VCVio/CryptoFoundations/FiatShamir.lean
  • VCVio/CryptoFoundations/Fork.lean
  • VCVio/OracleComp/QueryTracking/SeededOracle.lean
  • VCVio/OracleComp/QueryTracking/Structures.lean

Overview of Changes:
This diff provides a formal proof for the cryptographic forking lemma, a key result for proving the security of signature schemes.

Here is a summary of the key changes:

  • Formalizes the Forking Lemma: The central change is filling a sorry in Fork.lean with a complete proof of the main inequality of the forking lemma. This involves complex probabilistic reasoning over two executions of an algorithm with related random inputs.

  • Adds Seed Simulation Machinery: To enable the forking lemma proof, a significant number of powerful new lemmas are added to SeededOracle.lean. These lemmas formalize the properties of simulating oracle computations using pre-generated random "seeds", particularly showing how distributions behave when seeds are truncated or modified.

  • Introduces Mathematical Inequalities: A new file, ENNReal/SumSquares.lean, adds mathematical tools for extended non-negative reals, including a version of Jensen's inequality. These are used directly in the probabilistic arguments of the forking lemma.

  • Minor Proof Completion: A proof obligation (sorry) is completed in FiatShamir.lean, verifying the correctness of the Fiat-Shamir transformation's structure.

New 'sorry's: 0

@quangvdao
chore: add Quang Dao to author headers across 24 files
25b8aef 
Add co-authorship credit for substantial contributions across
OracleComp, EvalDist, CryptoFoundations, and Examples modules.

Made-with: Cursor
@quangvdao quangvdao changed the title feat(Fork): complete forking lemma proof feat(Fork): complete forking lemma proof with seeded oracle infrastructure Mar 1, 2026
@quangvdao quangvdao merged commit 01e4f41 into master Mar 1, 2026
3 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@quangvdao